es:ES, Qa, Rb:(EE), A, B:Type, Ia:AbsInterface(A), Ib:AbsInterface(B), f:(E(Ia)B),
g:(E(Ib)E).
g glues Ia:Qa f Ib:Rb  (g  E(Ib)E(Ia)) 

latex

Definitions

t  T, b, {I}, x:A  B(x), ES, x:AB(x), Type, AbsInterface(A), s = t, Q ==f== P, Q = f== P, f(a), f is Q-R-pre-preserving on P, Inj(A;B;f), P  Q, x:A. B(x), E(X), Top, EqDecider(T), Unit, left + right, IdLnk, Id, EOrderAxioms(E; pred?; info), EState(T), Knd, kindcase(k; a.f(a); l,t.g(l;t) ), Msg(M), type List, , , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), e < e', r  s, , constant_function(f;A;B), P & Q, let x,y = A in B(x;y), E, {x:A| B(x)} , t.1, x. t(x), S  T, , suptype(S; T), A c B, g glues Ia:Qa f Ib:Rb, e  X, pred!(e;e'), SWellFounded(R(x;y)), Void, x:A.B(x), first(e), A, loc(e), <a, b>, x,y. t(x;y), kind(e)

Lemmas

deq wf, EOrderAxioms wf, Id wf, kind wf, loc wf, Msg wf, nat wf, val-axiom wf, cless wf, qle wf, bool wf, rationals wf, Knd wf, kindcase wf, IdLnk wf, EState wf, constant function wf, not wf, first wf, unit wf, event system wf, es-E wf, top wf, assert wf, es-is-interface wf, Q-R-glues wf, weak-antecedent-surjection-property, es-interface-predicate wf, subtype rel function, subtype rel set, es-E-interface wf, subtype rel weakening, ext-eq weakening